(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)

(set-logic QF_NIA)

(declare-fun v0 () Int)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(declare-fun v3 () Int)
(declare-fun v4 () Int)
(declare-fun v5 () Int)
(declare-fun v6 () Int)
(declare-fun v7 () Int)
(declare-fun v8 () Int)
(declare-fun v9 () Int)

(assert
(let ((e14 (* v4 2)))
(let ((e15 (+ (- v2) e14)))
(let ((e16 (+ v5 v5)))
(let ((e17 (+ v7 e16)))
(let ((e18 (* v1 v8)))
(let ((e19 (- (- v3) v5)))
(let ((e20 (+ e14 v3)))
(let ((e21 (+ v1 v7)))
(let ((e22 (+ (- v3) e19)))
(let ((e23 (- e16 v7)))
(let ((e25 (+ (- v3) v7)))
(let ((e26 (+ v5 e15)))
(let ((e27 (+ e18 e19)))
(let ((e28 (- e25)))
(let ((e30 (- e17)))
(let ((e31 (- e30 v3)))
(let ((e32 (+ v5 e28)))
(let ((e33 (* e28 (- 2))))
(let ((e34 (* e14 (- 8))))
(let ((e38 (- e34)))
(let ((e39 (* (- 2) v8)))
(let ((e40 (- e28 v8)))
(let ((e41 (- e27 e40)))
(let ((e42 (* v6 2)))
(let ((e43 (+ e22 e40)))
(let ((e44 (- e26)))
(let ((e45 (+ e38 e21)))
(let ((e47 (+ v2 v0)))
(let ((e50 (- e27 (- v2))))
(let ((e52 (* e45 v8)))
(let ((e53 (+ (- v2) e16)))
(let ((e54 (* (- 2) e52)))
(let ((e55 (- e39)))
(let ((e56 (+ e18 e44)))
(let ((e58 (- e55 e42)))
(let ((e59 (+ e28 e50)))
(let ((e60 (- e43)))
(let ((e61 (- e30 e34)))
(let ((e65 (* e58 e43)))
(let ((e66 (* e20 e19)))
(let ((e76 (- e23)))
(let ((e78 (- e59)))
(let ((e90 (* v0 e39)))
(let ((e91 (+ e41 e47)))
(let ((e95 (- e31)))
(let ((e101 (* e66 e90)))
(let ((e102 (+ e91 e32)))
(let ((e103 (- e95 e61)))
(let ((e107 (- e38 e60)))
(let ((e119 (- e39)))
(let ((e122 (+ e78 e76)))
(let ((e124 (+ e58 e56)))
(let ((e129 (- e34)))
(let ((e147 (- e129 e42)))
(let ((e151 (* e101 e65)))
(let ((e155 (- e119 e102)))
(let ((e160 (* e155 e19)))
(let ((e163 (- e124)))
(let ((e172 (* e147 e122)))
(let ((e235 (- e33)))
(let ((e268 (* e78 e235)))
(let ((e272 (* 2 e163)))
(let ((e274 (+ e103 e151)))
(let ((e293 (- e18 e272)))
(let ((e632 (- e274)))
(let ((e692 (- e53 e268)))
(let ((e762 (- e692)))
(let ((e976 (* e293 e632)))
(let ((e3337 (< e107 36)))
(let ((e6944 (ite e3337 e762 e976)))
(> e6944 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
